\begin{tabbing}
$\forall$\=${\it es}$:ES, $e_{1}$:E, $e_{2}$:\{$e$:E$\mid$ loc($e$) $=$ loc($e_{1}$) $\in$ Id \}, $P$,\+
\\[0ex]$Q$:(\{$e$:E$\mid$ loc($e$) $=$ loc($e_{1}$) $\in$ Id \}$\rightarrow$Prop).
\-\\[0ex]($\forall$$e$:\{$e$:E$\mid$ loc($e$) $=$ loc($e_{1}$) $\in$ Id \}. $P$($e$) $\Leftrightarrow$ $Q$($e$)) $\Rightarrow$ ($\exists$$e$$\in$[$e_{1}$,$e_{2}$).$P$($e$) $\Leftrightarrow$ $\exists$$e$$\in$[$e_{1}$,$e_{2}$).$Q$($e$))
\end{tabbing}